import net.sf.javabdd.BDD;
import net.sf.javabdd.BDDFactory;

public class QueensLogic{
	private int x = 0;
    private int y = 0;
    private static final int nodeSize = 2000000; // As suggested in the project description
    private static final int cacheSize = 200000; // As suggested in the project description

    private int[][] board;						 // Board object having "0" for unfilled, "1" when queen is placed, and "-1" when queen cannot be placed 
    private BDD nQueens;						 // BDD that take in account new constraints made with insert actions
    private BDD[][] cellVariables;			 	 // Assigns to each cell on the board, a boolean variable, to be able to validate possible future movements
    private BDDFactory bddObject;

    public void initializeGame(int size) {
        this.x = size;
        this.y = size;
        this.board = new int[x][y];
        
        // Call step 1
        initBDD(); 				
        
        // Call step 2
        addRestrictionRules(); 	
        
        // Update the starting board, filling even from the beginning the invalid cells (that could not be used)
        updateValidDomainsAndBoard();
        
        // Print the number of possible solutions. Should print 10 for 5x5, 4 for 6x6, 92 for 8x8.
        System.out.println("N Queens satCount =  " + nQueens.satCount()); 
    }
   
    public int[][] getGameBoard() {
        return board;
    }

    public boolean insertQueen(int column, int row) {
    	// check if queen try to be put on an invalid cell
    	if (board[column][row] == -1 || board[column][row] == 1) {
            return false;
        }

        board[column][row] = 1;

        // Step 6
        applyInsert(column, row); 

        return true; // all remaining cells are valid
    }
    

    // Private members
    //
    // Step 1: Build n-queen BDD board
    //
    private void initBDD() {
        // Initialize BDD factory (library to be used)
        bddObject = BDDFactory.init(nodeSize, cacheSize);
        
        // set the number of BDD variables to be used
        bddObject.setVarNum(x*y);
        
        // Initialize the constraint variable to be used along the game
        nQueens = bddObject.one(); 
        
        // Initialize each cell on the board
        cellVariables = new BDD[x][y]; // Set the size of the board
        for(int i = 0; i < x; i++){
                for(int j = 0; j < y; j++){
                        cellVariables[i][j] = bddObject.ithVar((x*i) + j); // Define variable indices, to make them unique
                }
        }
    }
    
    // Step 2
    // Add the rules of the n-queen problem to the BDD of the board (i.e. restrict the board BDD with the rules of n-queen).
    // Each rule added has been commented accordingly 
    //
    private void addRestrictionRules() {
        setBoardRestrictions();       

        // Apply each cell restriction to main BDD variable
        for(int col = 0; col < x; col++) {
                for(int row = 0; row < y; row++) {
		                nQueens = nQueens.and(getCellRestrictions(col, row));
                }
        }
    }

    // This rules are more general, and not cell specific, being applied to multiple cells
    // It must be a queen in each row or column (singularity will be enforced by cell restriction function)
    //
	private void setBoardRestrictions() {
		// There must be a queen in each column
        for(int i = 0; i < x; i++) {
                BDD oneQueenPerColumn = bddObject.zero();
                for(int j = 0; j < y; j++) {
                        oneQueenPerColumn = oneQueenPerColumn.or(cellVariables[i][j]);
                }
                
                nQueens = nQueens.and(oneQueenPerColumn);
        }       
        
        // There must be a queen in each row
        for(int j = 0; j < y; j++) {
                BDD oneQueenPerRow = bddObject.zero();
                for(int i = 0; i < x; i++) {
                	oneQueenPerRow = oneQueenPerRow.or(cellVariables[i][j]);
                }
                
                nQueens = nQueens.and(oneQueenPerRow);
        }
	}

    // Retrieve rules to be followed by a specified cell
    //
	private BDD getCellRestrictions(int cellColumn, int cellRow) {
		// Boolean variable to hold the main expression for selected cell
		BDD cellRulesToApply = bddObject.one();
            
		// Rule1: No more than 1 queen in the same column
		for (int i = 0; i < y; i++) {
		        if(i != cellRow) {
		                BDD noMoreQueensonSameColumn = (cellVariables[cellColumn][cellRow].and(cellVariables[cellColumn][i])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensonSameColumn);
		        }
		}
		
		// Rule2: No more than 1 queen in the same row
		for (int i = 0; i < x; i++) {
		        if(i != cellColumn) {
		                BDD noMoreQueensOnSameRow = (cellVariables[cellColumn][cellRow].and(cellVariables[i][cellRow])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensOnSameRow);
		        }
		}
            
		// Rule3: No more than 1 queen in the same negative slope
		for (int i = 1; i < x; i++) {
		        int slopeColumn = cellColumn-i;
		        int slopeRow = cellRow-i;
		        
		        if(slopeColumn >= 0 && slopeRow >= 0) { // Down left
		                BDD noMoreQueensOnSameDiagonal = (cellVariables[cellColumn][cellRow].and(cellVariables[slopeColumn][slopeRow])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensOnSameDiagonal);
		        }
		        
		        slopeColumn = cellColumn+i;
		        if(slopeColumn < x && slopeRow >= 0) { // Down right
		                BDD noMoreQueensOnSameDiagonal = (cellVariables[cellColumn][cellRow].and(cellVariables[slopeColumn][slopeRow])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensOnSameDiagonal);
		        }
		}
		
		// Rule4: No more than 1 queen in the same positive slope
		for (int i = 1; i < x; i++) {
		        int slopeColumn = cellColumn + i;
		        int slopeRow = cellRow + i;
		        if(slopeColumn < x && slopeRow < y) { // Up right
		                BDD noMoreQueensOnSameDiagonal = (cellVariables[cellColumn][cellRow].and(cellVariables[slopeColumn][slopeRow])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensOnSameDiagonal);
		        }
		        
		        slopeColumn = cellColumn - i;
		        if(slopeColumn > 0 && slopeRow < y) { // Up left
		                BDD noMoreQueensOnSameDiagonal = (cellVariables[cellColumn][cellRow].and(cellVariables[slopeColumn][slopeRow])).not();
		                cellRulesToApply = cellRulesToApply.and(noMoreQueensOnSameDiagonal);
		        }
		}
		
		return cellRulesToApply;
	}    
    
    // Step 3: Get the assignment from the board
    // 
    private void applyInsert(int cellColumn, int cellRow) {        
    	// Execute the insertion in the BDD
        BDD selection = cellVariables[cellColumn][cellRow];
        nQueens = nQueens.and(selection); 
        
        // DEBUG: Print the remaining possible solutions
        System.out.println("N Queens satCount =  " + nQueens.satCount());
        
        //Update the board, marking as invalid all the future impossible movements
        updateValidDomainsAndBoard();
    }
    
    // Step 4+5     
    // Get the valid domains and update the board according to these
    //
    private void updateValidDomainsAndBoard() {
        for(int i = 0; i < x; i++) {
                for(int j = 0; j < x; j++) {
                        BDD test = nQueens.and(cellVariables[i][j]);
                        
                        // Being false then no solution exists, for this specific cell
                        if(test.isZero()) 
                           board[i][j] = -1;
                }
        }       
        
        // If only 1 solution exists, then fill remaining squares, and quicker complete the full configuration
        if(nQueens.satCount() == 1) {
            updateFullConfiguration();
        }
    }

    // In case there is only one solution, then fill blank squares and quicker complete the full configuration
    //
	private void updateFullConfiguration() {
		for(int currentRow = 0; currentRow < x; currentRow++) {
		        for(int j = 0; j < x; j++) {
		                if(board[currentRow][j] == 0) {
		                        board[currentRow][j] = 1;
		                }
		        }
		}
	}
}